The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
We provide simple conditions which allow us to conclude that in case of several well-known Prolog programs the unification algorithm can be replaced by iterated matching. The main tools used here are types and generic expressions for types. As already noticed by other researchers, such a replacement offers a possibility of improving the efficiency of program's execution.
Two transition systems are logically equivalent if they satisfy the same formulas of a given logic. For some of these logics, such as Hennessy-Milner's logic, there is an algebraic characterization of this equivalence involving particular homomorphisms of transition systems. This logical equivalence is associated with a preorder: a transition system S is less than S' if all formulas satisfied by S...
We describe a method for formally developing functional programs using the “propositions as types” paradigm. The idea is that a function together with its proof of correctness forms a morphism in a category whose objects are input/output specifications. The functionproof pairs, called “deliverables”, can be combined by the operations of a cartesian closed category, indeed by the same operations which...
The definition and some known results on complex traces are reviewed. We also discuss some open questions concerning the Posetproperty of complex traces. The main new contribution of the paper is the presentation of the notion of complex-like trace. Every complex trace is complex-like, but there are other objects such as a finite trace with some additional non-empty alphabetic information. In the...
Issues in the mathematical semantics of two restrictions of the λ-calculus, i.e. λI-calculus and λv-calculus, are discussed. A fully abstract model for the natural evaluation of the former is defined using complete partial orders and strict Scott-continuous functions. A correct, albeit non-fully abstract, model for the SECD evaluation of the latter is denned using Girard's coherence spaces and stable...
Action structures have previously been proposed as an algebra for both the syntax and the semantics of interactive computation. Here a class of concrete action structures called action calculi is identified, which can serve as a non-linear syntax for a wide variety of models of interactive behaviour. They generalise a previously defined action structure PIC for the π-calculus. One action calculus...
The research reported in this paper is concerned with the problem of reasoning about properties of higher order functions involving state. It is motivated by the desire to identify what, if any, are the difficulties created purely by locality of state, independent of other properties such as side-effects, exceptional termination and non-termination due to recursion. We consider a simple language (equivalent...
We view the Chu space interpretation of linear logic as an alternative interpretation of the language of the Peirce calculus of binary relations. Chu spaces amount to K-valued binary relations, which for K=2n we show generalize n-ary relational structures. We also exhibit a four-stage unique factorization system for Chu transforms that illuminates their operation.
The notion of a dynamic labeled 2-structure is introduced and investigated. It generalizes the notion of a labeled 2-structure (ℓ2s), see [ER1], by making it possible to change the (label) relationships between the nodes. This is achieved by storing in the nodes of a ℓ2s output and input functions which can change the outgoing and incoming labels, respectively. The notion of a clan which is central...
We first introduce the notion of a general primality type, for a systematic study of “simple”, “primitive” or “prime” solutions of the Post Correspondence Problem. We give an exhaustive charcterization of general primality types. We then introduce PCP-related complexity classes, for instance, the time complexity classes PCP-P and PCP-NP. We obtain the chain of inclusions $$P \subseteqq PCP -...
This tutorial paper provides an introduction to intuitionistic logic and linear logic, and shows how they correspond to type systems for functional languages via the notion of ‘Propositions as Types”. The presentation of linear logic is simplified by basing it on the Logic of Unity. An application to the array update problem is briefly discussed.
We consider the following problem: Given ordered labeled trees S and T can S be obtained from T by deleting nodes ? Deletion of the root node u of a subtree with children (T1,..., Tn) means replacing the subtree by the trees T1,...,Tn. For the tree inclusion problem,there can generally be exponentially many ways to obtain the included tree. Recently, P.Kilpeläinen...
We consider a fixed point extension of the second order lambda calculus equipped with a call by value evaluation mechanism. We interpret the language in a partial cartesian closed category of “directed complete” partial equivalence relations (pers) over a domain theoretic model of a type-free, call-by-value, lambda calculus. Our main result is that the notions of “syntactic” and “semantic” convergence...
We investigate the complexity of sets that have a rich internal structure and at the same time are reducible to sets of either low or very high information content. In particular, we show that every length-decreasing or word-decreasing self-reducible set that reduces to some sparse set via a non-monotone variant of the Hausdorff reducibility is low for Δ2p. Measuring the...
Operational (O) and denotational (D) semantic models are designed for a language incorporating a version of the UNIX fork and pipe commands. Taking a simple while language as starting point, a number of programming constructs are added which achieve that a program can generate a dynamically evolving linear array of processes connected by channels. Over these channels sequences of values (‘streams’)...
We incorporate finite monoids into the theory of Rabin recognizability of infinite tree languages. We define a free monoid of infinite trees and associate with each infinite tree language L a language L of infinite words over this monoid. Using this correspondence we introduce strong monoid recognizability of infinite tree languages (strengthening the standard notion for infinite words) and show that...
The complexity of type reconstruction for simply-typed lambda calculus with subtype relation resulting from single inheritance (i.e. being a disjoint union of tree-like posets) is analyzed. As a result a class of posets including (but not restricted to) trees is defined, for which the said problem is solvable in polynomial time.
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.